dtmc

//the length of the backoff stage
const int w=8;
const int q_max=1;

module SQ
	done : [0..1] init 0;
	// q = number of requests currently in queue
	q : [0..q_max] init 0;
	
	// A request arrives
	[request] done=0 -> 0.2739 : (q'=min(q+1,q_max)) & (done'=1) + (1-0.2739) : (done'=1);
	// A request is served
	[serve] q>0 -> 1 : (q'=q-1);

        [step] true -> 1 : (done'=0);
	// Last request is served
	//[serve_last] q=1 -> (q'=q-1);
	
endmodule

// module for process 1
module carA
    backoffA : [0..w-1] init 1;

    //Indicate that A is sending a message, which is done whenever the backoff phase is 0
    sendA : [0..1] init 0;
    
    //[request] true -> 1 : (sendA'=(backoffA=0 ? 1 : 0));
	
    //make the model work for w upto 40
    //calculate the probability to reach a certain backoff state
    //The car sends a message whenever the transition to backoff state 0 is made
    [serve] backoffA=0 -> 1 : (sendA'=1);

    [step] done=1 & backoffA=0 & sendA=1 -> 
			( w>0 ? 1 : 0 )*1/w:(backoffA'=0) & (sendA'=0) + 
			( w>1 ? 1 : 0 )*1/w:(backoffA'=1) & (sendA'=0) + 
			( w>2 ? 1 : 0 )*1/w:(backoffA'=2) & (sendA'=0) + 
			( w>3 ? 1 : 0 )*1/w:(backoffA'=3) & (sendA'=0) + 
			( w>4 ? 1 : 0 )*1/w:(backoffA'=4) & (sendA'=0) + 
			( w>5 ? 1 : 0 )*1/w:(backoffA'=5) & (sendA'=0) + 
			( w>6 ? 1 : 0 )*1/w:(backoffA'=6) & (sendA'=0) + 
			( w>7 ? 1 : 0 )*1/w:(backoffA'=7) & (sendA'=0) + 
			( w>8 ? 1 : 0 )*1/w:(backoffA'=8) & (sendA'=0) + 
			( w>9 ? 1 : 0 )*1/w:(backoffA'=9) & (sendA'=0) + 
			( w>10 ? 1 : 0 )*1/w:(backoffA'=10) & (sendA'=0) + 
			( w>11 ? 1 : 0 )*1/w:(backoffA'=11) & (sendA'=0) + 
			( w>12 ? 1 : 0 )*1/w:(backoffA'=12) & (sendA'=0) + 
			( w>13 ? 1 : 0 )*1/w:(backoffA'=13) & (sendA'=0) + 
			( w>14 ? 1 : 0 )*1/w:(backoffA'=14) & (sendA'=0) + 
			( w>15 ? 1 : 0 )*1/w:(backoffA'=15) & (sendA'=0) + 
			( w>16 ? 1 : 0 )*1/w:(backoffA'=16) & (sendA'=0) + 
			( w>17 ? 1 : 0 )*1/w:(backoffA'=17) & (sendA'=0) + 
			( w>18 ? 1 : 0 )*1/w:(backoffA'=18) & (sendA'=0) + 
			( w>19 ? 1 : 0 )*1/w:(backoffA'=19) & (sendA'=0);
    [step] done=1 & backoffA=0 & sendA=0 & q=0 -> 1 : (backoffA'=0);

    [step] done=1 & backoffA>0 -> 1: (backoffA'=backoffA-1);

    //[step] done=1 & backoffA>0 & (sendA+sendB+sendC>0) -> 1: (backoffA'=backoffA);
    //[step] done=1 & backoffA>0 & (sendA+sendB+sendC=0) -> 1: (backoffA'=backoffA-1);
endmodule

// add further processes through renaming
module carB = carA[backoffA=backoffB, sendA=sendB, request=requestB, q=qB, serve=serveB, done=doneB] endmodule
module carC = carA[backoffA=backoffC, sendA=sendC, request=requestC, q=qC, serve=serveC, done=doneC] endmodule

module SQB = SQ[q=qB, request=requestB, serve=serveB, done=doneB] endmodule
module SQC = SQ[q=qC, request=requestC, serve=serveC, done=doneC] endmodule

rewards "successfultransmission"
	[step] sendA + sendB + sendC = 1 : 1;
endrewards

rewards "collision"
	[step] sendA + sendB + sendC > 1 : 1;
endrewards

rewards "radiosilence"
	[step] sendA + sendB + sendC = 0 : 1;
endrewards

rewards "sendA"
	[step] sendA =1 : 1;
endrewards

rewards "sendB"
	[step] sendB =1 : 1;
endrewards

rewards "sendC"
	[step] sendC =1 : 1;
endrewards